theory REQ_SEC
imports Main "../GPTEE_Instantiation" "./Memory_SEC" "./TEE_IPC_SEC" "./TEEC_IPC_SEC"
begin
section "syscall proof"
lemma syscall_integrity:
    assumes p1: "a = sys Reserved"
    shows "∀ d s s'. reachable0 s ∧ ((the (domain_of_event s a)) ∖↝ d) ∧ (s, s') ∈ exec_event a  ⟶ (s ∼ d ∼ s')"
  
proof -
 {
  fix s s' d 
  assume a1: "reachable0 s"
  assume a2: "((the (domain_of_event s a)) ∖↝ d)"
  assume a3: "(s,s') ∈ exec_event a"
  have "s'=s" using exec_event_def a3 p1 by simp
  then have "s∼ d ∼ s'" by auto
}
 then show ?thesis by blast
 qed

lemma syscall_integrity_e:
   "integrity_e (sys Reserved)"
    using syscall_integrity integrity_e_def
    by auto


lemma syscall_weak_confidentiality:
  assumes p1: "a = sys Reserved"
  shows "∀ d s t.
           reachable0 s ∧
           reachable0 t ∧
           (s ∼ d ∼ t) ∧
           ((domain_of_event s a) = (domain_of_event t a)) ∧
           (exec_prime s=exec_prime t)∧
           ((the (domain_of_event s a)) ↝ d) ∧
           (s ∼ (the (domain_of_event s a)) ∼ t) ⟶
           (∀ s' t'. (s, s') ∈ exec_event a ∧ (t, t') ∈ exec_event a ⟶ (s' ∼ d ∼ t'))"

proof -
  {
    
    fix s t d s' t'
    assume a1:"reachable0 s"
    assume a2:"reachable0 t"
    assume a3:"s∼d∼t"
    assume a31:"exec_prime s=exec_prime t"
    assume a4:"(domain_of_event s a) = (domain_of_event t a)"
    assume a5:"(the (domain_of_event s a)) ↝ d"
    assume a6:"s ∼ (the (domain_of_event s a)) ∼ t"
    assume a7:"(s, s') ∈ exec_event a"
    assume a8:"(t, t') ∈ exec_event a"
    have b1:"s'=s" using a7 p1 exec_event_def by auto
    have b2:"t'=t" using a8 p1 exec_event_def by auto
    then have "(s' ∼ d ∼ t')" using b1 b2 a3 by blast
  }
  then show ?thesis by blast 
qed

lemma syscall_weak_confidentiality_e:
   "weak_confidentiality_e (sys Reserved)"
    using syscall_weak_confidentiality weak_confidentiality_e_def get_exec_prime_def
    by (smt (verit, del_insts) Pair_inject)

section "requirement layer integrity"

theorem req_integrity : integrity

proof -
  {
  fix a
  have "integrity_e a"
  proof(induct a)
    case (hyperc x)
    show ?case 
      using TEEC_InitializeContext_integrity_e TEEC_FinalizeContext_integrity_e
            TEEC_OpenSession1_integrity_e TEEC_OpenSession2_integrity_e
            TEEC_OpenSession3_integrity_e TEEC_OpenSession4_integrity_e TEEC_CloseSession1_integrity_e
            TEEC_CloseSession2_integrity_e TEEC_CloseSession3_integrity_e TEEC_CloseSession4_integrity_e
            TEEC_InvokeCommand1_integrity_e TEEC_InvokeCommand2_integrity_e
            TEEC_InvokeCommand3_integrity_e TEEC_InvokeCommand4_integrity_e TEEC_RegisterSharedMemory_integrity_e
            TEEC_AllocateSharedMemory_integrity_e
            TEEC_ReleaseSharedMemory_integrity_e TEE_OpenTASession1_integrity_e
            TEE_OpenTASession2_integrity_e TEE_OpenTASession3_integrity_e TEE_OpenTASession4_integrity_e
            TEE_InvokeTACommand1_integrity_e TEE_InvokeTACommand2_integrity_e
            TEE_InvokeTACommand3_integrity_e TEE_InvokeTACommand4_integrity_e TEE_CloseTASession1_integrity_e
            TEE_CloseTASession2_integrity_e TEE_CloseTASession3_integrity_e TEE_CloseTASession4_integrity_e
            TEE_CheckMemoryAccessRights_integrity_e
            TEE_Malloc_integrity_e TEE_Realloc_integrity_e
             TEE_Free_integrity_e  
           apply (rule Hypercall.induct)
        done 
    next
    case (sys x)
    show ?case using syscall_integrity_e GPTEE_Instantiation.Syscall.induct by simp
    qed
    }
    then show ?thesis by fastforce
qed


section "requirement layer confidentiality"

theorem req_weak_confidentiality : weak_confidentiality

proof -
{
  
  fix a
  have "weak_confidentiality_e a"
  proof(induct a)
    case (hyperc x)
    show ?case 
       using TEEC_InitializeContext_weak_confidentiality_e TEEC_FinalizeContext_weak_confidentiality_e
            TEEC_OpenSession1_weak_confidentiality_e TEEC_OpenSession2_weak_confidentiality_e
            TEEC_OpenSession3_weak_confidentiality_e TEEC_OpenSession4_weak_confidentiality_e TEEC_CloseSession1_weak_confidentiality_e
            TEEC_CloseSession2_weak_confidentiality_e TEEC_CloseSession3_weak_confidentiality_e TEEC_CloseSession4_weak_confidentiality_e
            TEEC_InvokeCommand1_weak_confidentiality_e TEEC_InvokeCommand2_weak_confidentiality_e
            TEEC_InvokeCommand3_weak_confidentiality_e TEEC_InvokeCommand4_weak_confidentiality_e TEEC_RegisterSharedMemory_weak_confidentiality_e
            TEEC_AllocateSharedMemory_weak_confidentiality_e
            TEEC_ReleaseSharedMemory_weak_confidentiality_e TEE_OpenTASession1_weak_confidentiality_e
            TEE_OpenTASession2_weak_confidentiality_e TEE_OpenTASession3_weak_confidentiality_e TEE_OpenTASession4_weak_confidentiality_e
            TEE_InvokeTACommand1_weak_confidentiality_e TEE_InvokeTACommand2_weak_confidentiality_e
            TEE_InvokeTACommand3_weak_confidentiality_e TEE_InvokeTACommand4_weak_confidentiality_e TEE_CloseTASession1_weak_confidentiality_e
            TEE_CloseTASession2_weak_confidentiality_e TEE_CloseTASession3_weak_confidentiality_e TEE_CloseTASession4_weak_confidentiality_e
            TEE_CheckMemoryAccessRights_weak_confidentiality_e
            TEE_Malloc_weak_confidentiality_e TEE_Realloc_weak_confidentiality_e
             TEE_Free_weak_confidentiality_e  
            apply (rule Hypercall.induct)
        done     
    next
    case (sys x)
    show ?case using  syscall_weak_confidentiality_e GPTEE_Instantiation.Syscall.induct by simp
    qed
}
    then show ?thesis by fastforce
qed

theorem req_confidentiality : confidentiality
  using req_weak_confidentiality req_integrity weak_with_step_cons
  by blast

end